#ifndef PDT_Z3_GRAPHVISITOR_H
#define PDT_Z3_GRAPHVISITOR_H

#include "PDTGraphVisitor.h"

#include <z3.h>

#include <vector>
#include <map>
#include <stack>
using namespace std;

//added because of circular includes
class PDTNode;
class PDTCodeGraph;

/*
 ;       int x,y,z;                      c0
 ;       x = y+z;                        s1,c1
 ;       y = y-1;                        s2, c2
 ;       if (y<z){                       b1
 ;       _if1
 ;               x = x +1;               s3, c3
 ;               if (x>3){               b2
 _if2
 ;                       y=x-z;  s4, c4
 ;                       z=z-1;  s5, c5
 ;               }
 _endif2
 ;       z= z-1;
 ;       } else {
 _else1
 ;       y=3;
 ;       }
 ;       _endif1
 ;       assert (x>y+z);         b3

 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

 (declare-sort Var)
 (declare-sort statement)
 (declare-fun E (statement) Int)         ; execution time function
 ; the definition of E is by declaring execution order across all program statements.

 (declare-fun inGamma (Var statement) Bool)      ; checks whether statement belongs to Gamma(variable)
 ;The definition of inGamma is by statement later on.

 (declare-const Start statement)
 (declare-const Infinity statement)
 (declare-const s0 statement)

 ;;;;;;;;;;;;;;;;;;;;;;;;
 ; isMaxBefore returns true if sT is the most recent statement updating v before s
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (define-fun isMaxBefore ((v Var) (sS statement) (sT statement)) Bool
 ((and (inGamma v sT) (<= (E sT) (E sS)) (forall (s statement) (=> (inGamma v s) ((=> (< (E s) (E sS)) (<= (E s) (E sT)))))))))

 ;;;;;;;;;;;;;;;;;;;;;;;;
 ;  VAL takes variable and current time and returns most recent statement
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (declare-fun VAL (Var Int) statement)
 (assert (forall (s statement) (v Var) (=> (not (= s s0)) ((isMaxBefore v s (VAL v (E s)))))))

 ;;;;;;;;;;;;;;;;;;;;;;;;
 ; s2i returns the value of a statement AND Vs2i return the value of a variable in a statement
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (declare-fun s2i (statement) Int)

 ;The definition of s2i is by statement later on.

 (define-fun Vs2i ((v Var) (s statement)) Int ((s2i (VAL v (E s)) ) ))

 ;;;;;;;;;;
 ; now declare the variables, the statements, and populate the functions
 ;   inGamma and s2i
 (declare-const x Var)
 (declare-const y Var)
 (declare-const z Var)

 (declare-const b1 statement)
 (declare-const b2 statement)
 (declare-const b3 statement)

 (declare-const s0 statement)
 (declare-const s1 statement)
 (declare-const s2 statement)
 (declare-const s3 statement)
 (declare-const s4 statement)
 (declare-const s5 statement)
 (declare-const s6 statement)

 (declare-const _if1 statement)
 (declare-const _else1 statement)
 (declare-const _endif1 statement)
 (declare-const _if2 statement)
 (declare-const _endif2 statement)


 ;;;;;;;;        declare partial order   ;;;;;;;;;;

 (assert (= (E Start) (+ (E s0) 0)))
 (assert (= (E Infinity) (+ (E b3) 1)))

 (assert (> (E s1) (E s0)))
 (assert (> (E s2) (E s1)))
 (assert (> (E b1) (E s2)))
 (assert (> (E _if1) (if (= (s2i b1) 1) (E b1) (E Infinity))))
 (assert (> (E s3) (E _if1)))
 (assert (> (E b2) (E s3)))
 (assert (> (E _if2) (if (= (s2i b1) 1) (E b2) (E Infinity))))
 (assert (> (E s4) (E _if2)))
 (assert (> (E s5) (E s4)))
 (assert (> (E _endif2) (if (= (s2i b2) 1) (E s5) (E b2))))
 (assert (> (E _else1) (if (= (s2i b1) 0) (E b1) (E Infinity))))
 (assert (> (E s6) (E _else1)))
 (assert (> (E _endif1) (if (= (s2i b1) 0) (E s6) (E b1))))
 (assert (> (E b3) (E _endif1)))




 ;;;;;;;;        initialize inGamma      ;;;;;;;;;


 (define-fun inGamma ((v Var) (s statement)) Bool (or
 (and (= v x) (= s s1))
 (and (= v x) (= s s3))
 (and (= v y) (= s s2))
 (and (= v y) (= s s4))
 (and (= v z) (= s s5))
 ))

 ;;;;;;  initialize s2i
 (assert (= (s2i s1) (+ (Vs2i y s1) (Vs2i z s1))))
 (assert (= (s2i s2) (- (Vs2i y s2) 1)))
 (assert (= (s2i b1) ((if (< (Vs2i y b1) (Vs2i z b1)) 1 0))))
 (assert (= (s2i s3) (+ (Vs2i x s3) 1) ))
 (assert (= (s2i b2) (if (> (Vs2i x b2) 3) 1 0)))
 (assert (= (s2i s4) (- (Vs2i x s4) (Vs2i z s4))))
 (assert (= (s2i s5) (- (Vs2i z s5) 1)))
 (assert (= (s2i s6) (- (Vs2i x s6) 2)))
 (assert (= (s2i b3) (if (> (Vs2i x b3) (+ (Vs2i y b3) (Vs2i z b3))) 1 0)))


 (check-sat)
 (model)
 (eval (inGamma x s5))
 (eval true)
 */

class PDTZ3Visitor : public PDTGraphVisitor
{
private:

  class PrepQuantifier
  {
      public:
#define MAXPATTERNS  8
    /*
     * IN case of nested while statements, the visitor holds the current while-depth.
     * We translate every code statement in a while loop into a depth-dimension array of statements in Z3.
     * This function returns an array of quantifier bound variables that we use to select the statements.
     * For example consider statement s and t in the following
     *   while () { ... while() {  ... s t ...  } }
     * s and t will be translated into Array of Array of Statement
     * and we need to say something like
     * forall i forall j. e(s(i][j]) < e(t[i][j]).
     *
     * The following function declares the i and j variables if depth was 2.
     *
     */
  public:
    unsigned int maxWhileDepth;
    unsigned int weight;

    unsigned numPatterns;
    Z3_pattern * patterns;

    unsigned numDecls;
    Z3_sort * sorts;
    Z3_symbol * declNames;
    Z3_ast * iterators;

    Z3_ast body;

    PrepQuantifier(unsigned int maxWhileDepth);
    virtual ~PrepQuantifier();

    void
    clear();
    Z3_ast
    makeForall(PDTZ3Visitor & ZV);
    Z3_ast
    makeExists(PDTZ3Visitor & ZV);
    void
    prepareIterators(PDTZ3Visitor & ZV);
    Z3_ast
    makeSelect(PDTZ3Visitor & ZV, Z3_ast arrOfStatements);
  };

public:

  unsigned int counter; // TODO: number of nodes traversed so far
  unsigned int boundCounter;

  Z3_config config;
  Z3_context ctx;

  Z3_sort Int;
  Z3_sort Bool;
  Z3_sort Statement;
  Z3_sort Var;
  Z3_sort * ArrayOfStatements;

  Z3_ast Start;
  Z3_func_decl fStart;
  Z3_ast Infinity;
  Z3_func_decl fInfinity;

  Z3_ast True;
  Z3_ast False;
  Z3_ast Zero;

  Z3_ast current; // intermediary node to keep track of the latest statement in the traversal

  Z3_func_decl E;// function that takes a statement and returns its execution time

  Z3_func_decl * eOrder; // array of functions that force execution time order between <arrays> of statements 
                         // eOrder[i](s1, s2) == true means that s1 and s2 are i dimensional arrays of statements
                         // and E(s1[j_1]...[j_i]) < E(s2[j_1]...[j_i]

  Z3_func_decl * InGamma;// array of functions that takes a i-dimensional array of statements 
                         // and a variable and returns true if the statements assign to the variable

  Z3_func_decl IV; // function that takes a variable and returns its initial value (value at Start)

  Z3_func_decl * s2i;// function that takes a statement and returns its value
  Z3_func_decl Vs2i;// function that takes a variable and a statement and returns the variable's value in this statement
  Z3_func_decl VAL;// function that takes a variable and the statement's execution time and returns the most recent affecting statement
  Z3_func_decl isMaxBefore;// function that takes a variable v and two statements sS and sT, and returns true if sT is the most recent statement updating v before sS

  PrepQuantifier prepQuant;

  vector<Z3_ast*> Z3variables;
  vector<Z3_ast*> Z3constants;

  PDTNode * currentNode;
  PDTCodeGraph & CG;

  PDTZ3Visitor(PDTCodeGraph &aCG);
  virtual
  ~PDTZ3Visitor();

  Z3_ast
      makeBound(Z3_sort t, Z3_symbol & vName);


  void
  setup();
  void
  buildTypesAndConstants();
  void
  declareExecutionTimeFunction();
  void
  declareInGamma();
  void
  declareAndDefineIsMaxBefore();
  void
  declareAndDefineVal();
  void
  declareStatementToNumberValueFunction();
  void
  declareAndDefineVariableStatementToInt();
  void
  declareExecutionTimeFunctions();

  typedef enum {
      Unsat, Sat, None
  } Sat_Em;
  Sat_Em
      check() ;
  void
      toString() ;

  // helper functions

  Z3_ast 
  Z3ParseSMTLibString(const char * funcDef, 
        unsigned int nSorts, Z3_sort sorts[], 
        unsigned int nDecls, Z3_func_decl decls[],
        const char * funcName=NULL);

  Z3_ast
  mk_var(Z3_context ctx, const char * name, Z3_sort ty);

  Z3_ast
  makeStatement(const char *);

  char *
  makeName(const char * prefix, int i = 0);

  Z3_sort
  makeArrayOfStatementsSort(int dimension);

  Z3_ast
  makeArrayOfStatements(int dimension, const char * name);

  void
  assertOrder(Z3_ast s1, Z3_ast s2);

  void
  assertConditionalOrder(Z3_ast condition, Z3_ast target, Z3_ast _if,
      Z3_ast _else);

  Z3_ast
  mk_unary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x);
  Z3_ast
  mk_binary_app(Z3_context ctx, Z3_func_decl f, Z3_ast x, Z3_ast y);

  virtual bool pre(PDTNode*){return true;}
  virtual bool beforeChild(PDTNode*, PDTNode*, unsigned int){return true;}
  virtual bool afterChild(PDTNode*, PDTNode*, unsigned int){return true;}
  virtual bool post(PDTNode*){return true;}

};

#endif // PDT_Z3_GRAPHVISITOR_H
